T:(IdType), tab:secret-table(T), keyv:(:( + Atom1)  data(T)).
encrypt(tab;keyv)  secret-table(T) 

latex

Definitions	t  T, #$n, x:A. B(x), A  B, n+m, a < b, Void, x:AB(x), P  Q, False, A, , {x:A| B(x)} , , data(T), Atom$n, left + right, Type, x:A  B(x), {i..j}, <a, b>, , True, i z j, b, b, , s = t, P & Q, i  j < k, f(a), x.A(x), x. t(x), t.1, (i = j), f[x:=v], i <z j, T, P  Q, P  Q, Unit, encrypt(tab;keyv), secret-table(T), Id
Lemmas	secret-table wf, Id wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, update wf, eq int wf, pi1 wf, bool wf, bnot wf, assert wf, le int wf, int seg wf, nat wf, data wf, le wf